<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
          "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
  <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1" />
  <title>KLEE - Getting Started</title>
  <link type="text/css" rel="stylesheet" href="menu.css" />
  <link type="text/css" rel="stylesheet" href="content.css" />
</head>
<body>

<!--#include virtual="menu.html.incl"-->

<div id="content">

<h1>Getting Started: Building and Running KLEE</h1>

<!-- <p>FIXME: Intro and disclaimer.</p> -->

<h2 id="build">Building KLEE</h2>

<p>If you would like to try KLEE, the current procedure for building is
below.</p>
KLEE is built on LLVM; the first steps are to get a working LLVM
installation. See <a href="http://llvm.org/docs/GettingStarted.html">Getting
Started with the LLVM System</a> for more information.

<p><b>NOTE:</b> KLEE is only currently tested on Linux and Darwin x86-32
targets, using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g.,
2.5). We are currently working on full support for Linux and Darwin x86-64
targets.<p>

<ol>
  <li>Install llvm-gcc:
    <ul>
      <li>Download and install the LLVM 2.6 release of <tt>llvm-gcc</tt>
        from <a href="http://llvm.org/releases/download.html">here</a>.  Add
        <tt>llvm-gcc</tt> to your <tt>PATH</tt>. It is important to do this first
        so that <tt>llvm-gcc</tt> is found in subsequent <tt>configure</tt>
        steps. <tt>llvm-gcc</tt> will be used later to compile programs that KLEE
        can execute.</li>
    </ul>
  </li>

  <li><a href="http://llvm.org/releases/download.html#2.6">Download and build
      LLVM 2.6</a> (you may also use SVN head, but klee may not always be
      up-to-date with LLVM API changes).
    
    <div class="instr">
      $ curl -O http://llvm.org/releases/2.6/llvm-2.6.tar.gz <br>
      $ tar zxvf llvm-2.6.tar.gz <br>
      $ cd llvm-2.6 <br>
      $ ./configure --enable-optimized <br>
      $ make
    </div>
    
    (the <tt>--enable-optimized</tt> configure argument is not necessary, but
    KLEE runs very slowly in Debug mode).
  </li>
  
  <li>Checkout KLEE (to any path you like):
    <div class="instr">
      $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
    </div>
  </li>
  
  <li>Configure KLEE (from the KLEE source directory): 
    <div class="instr">
      $ ./configure --with-llvm=<i>path/to/llvm</i>
    </div>
    
    <p>This assumes that you compiled LLVM in-place.  If you used a
      different directory for the object files then use:
      <div class="instr">
	$ ./configure --with-llvmsrc=<i>path/to/llvm/src</i> --with-llvmobj=<i>path/to/llvm/obj</i>
      </div>
  </li>

  <li>Build KLEE (from the KLEE source directory):
    <div class="instr">
      $ make ENABLE_OPTIMIZED=1
    </div>
  </li>

  <li>Run the regression suite to verify your build:
    <div class="instr">
      $ make check<br>
      $ make unittests<br>
    </div>
  </li>

  <li>You're ready to go!  Go to the <a href="Tutorials.html">Tutorials</a> page
  to try KLEE.</li>
</ol>

<h2 id="uclib">Building KLEE with POSIX runtime support</h2>

<p>The steps above are enough for building and testing KLEE on closed programs
(programs that don't use any external code such as C library
functions). However, if you want to use KLEE to run real programs you will want
to enable the KLEE POSIX runtime, which is built on top of the uClibc C
library.</p>

<ol>
  <li>Download KLEE's uClibc:
    <ul>
      <li>
        KLEE uses a version of <a href="http://uclibc.org">uClibc</a> which has
        been modified slightly for use with KLEE. It is available for download
        here: <a href="http://t1.minormatter.com/~ddunbar/klee-uclibc-0.01.tgz">klee-uclibc-0.01.tgz</a>.
      </li>
    </ul>
  </li>
  
  <li>Build uClibc with <tt>llvm-gcc</tt>:
    <div class="instr">
      $ tar zxvf klee-uclibc-0.01.tgz <br>
      $ ./configure --with-llvm=<i>path/to/llvm</i> <br>
      $ make <br>
    </div>

    <p><b>NOTE:</b> KLEE's uClibc is shipped in a pre-configured for x86-32. If
      you are on a different target (e.g. x86-64), you will need to run 'make
      config' and select the correct target. The defaults for the other uClibc
      configuration variables should be fine.<p>
  </li>

  <li>Configure KLEE with uClibc/POSIX support:
    <div class="instr">
      $ ./configure --with-llvm=<i>path/to/llvm</i> --with-uclibc=<i>path/to/klee-uclibc</i> --enable-posix-runtime
    </div>
  </li>

  <li>Rebuild KLEE and run <tt>make check</tt> and verify that the POSIX tests
    run correctly.
  </li>
</ol>

</div>
</body>
</html>
